FDL - Nuprl Lemma : conditional-send1-p

Nuprl Lemma : conditional-send1-p_wf

11,40

k:Knd, T, A, B:Type, l:IdLnk, x, tg:Id, f:(A

T), c:(A

), es:ES.

k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v)

Definitions x:A. B(x), P Q, P & Q, A c B, k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v), , t T, x:A. B(x), {T}

Lemmas Knd wf, IdLnk wf, Id wf, bool wf, event system wf, not wf, es-kind-rcv, es-sender wf, es-val wf, es-vartype wf, es-when wf, assert wf

Definitions	x:A. B(x), P Q, P & Q, A c B, k(v:B) sends f(x:A,v) on l tagged with tg:T provided c(x,v), , t T, x:A. B(x), {T}
Lemmas	Knd wf, IdLnk wf, Id wf, bool wf, event system wf, not wf, es-kind-rcv, es-sender wf, es-val wf, es-vartype wf, es-when wf, assert wf